<html>
    <head>
        <title></title>
        <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
        <link rel="stylesheet" type="text/css" href="../style.css">
    </head>
    <body>
        <div class="text">
        <h2>Propagator</h2>
        After starting the propagator a new file named "Prop_package_procedure.adb" is 
        created in the same directory as the source file. This file contains exactly the same
        as the tab "Propagated". The following is necessary:
        <ul>
            <li> for the whole program there is a pre- and a post-condition</li>
            <li> right before a while-loop there is a invariant</li>
            <li> right before an if-command there is an assertion too
        </ul>
        Under this circumstances the program can generate a completly annotated program by
        using the rules of Hoare.<br />
        <br />
        The output matches the Mini-Ada syntax and is printed with logical tabulators.
        That way it can be easily opened in an Ada-compiler to work with the file further more.
        </div>
    </body>
</html>
